es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, p,
q:({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
[e1;e2]~([a,b].p(a,b))*[a,b].q(a,b)  Prop 

latex

Definitions	t  T, A & B, , x:A. B(x), AB, P & Q, i  j < k, P  Q, False, A, {i..j}, pred(e), E, Id, loc(e), Prop, x(s1,s2), (e <loc e'), e  e' , x:A. B(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), ES, P  Q, b, x. t(x), P  Q, P  Q, 1of(t), True, T
Lemmas	squash wf, true wf, int seg properties, nat plus properties, es-le-loc, es-loc-pred, or functionality wrt iff, all functionality wrt iff, es-locl-iff, event system wf, nat plus wf, es-le wf, es-locl wf, es-E wf, Id wf, es-loc wf, int seg wf, es-pred wf, le wf